\begin{tabbing}
((Unfold `decidable` 3 THEN InstHyp [$b$;$a$] 3 
\\[0ex]THENM InstHyp [$a$;$b$] 7 
\\[0ex]T\=HENM ProveProp) \+
\\[0ex]
\\[0ex]CollapseTHEN ((Auto\_aux (first\_nat 1:n) ((first\_nat 1:n),(first\_nat 3:n)) (first\_tok :t
\-\\[0ex]) inil\_term)))$\cdot$
\end{tabbing}